nLab extensional relation

Redirected from "strongly extensional quotient".
Extensional relations

Extensional relations

Idea

Given an extensional relation \prec on a set, two elements are equal if they cannot be distinguished by the structure of the set of elements that they are related to, that those elements are related to, and so on forever in one direction. We generally think of xyx \prec y as saying that xx is a ‘member’ of yy, so that \prec is extensional when “xx is determined by its members” as in the axiom of extensionality for material set theory.

Definitions

We begin with the historically first definition, which is correct for well-founded relations. We then consider ways to extend this to more general relations, where the last version seems to be most correct.

Weak extensionality

A relation \prec on a set SS is weakly extensional if, given any elements xx and yy of SS, x=yx = y whenever (for all tt) txt \prec x if and only if tyt \prec y.

Interpreting \prec as membership \in, this corresponds to the axiom of extensionality as usually stated for pure sets. However, it is really only appropriate when \prec is well-founded, just as the usual axiom of extensionality must be strengthened in the absence of the axiom of foundation.

However, when \prec is well-founded, weak extensionality is equivalent to all the stronger notions below; thus in that case it is usually called just extensionality.

Finsler extensionality

Let *\prec^* be the reflexive-transitive closure of the relation \prec on SS (so *\prec^* is a preorder). Given an element yy of SS, let S *yS \downarrow^* y be the downset of yy under *\prec^*:

S *y={x:S|x=t 0t n=y} S \downarrow^* y = \{ x: S \;|\; x = t_0 \prec \cdots \prec t_n = y \}

with n0n \geq 0. Note that yy itself belongs to S *yS \downarrow^* y (through n=0n = 0, if in no other way), so we may take it to be a pointed set. Then \prec is Finsler-extensional if it is weakly extensional and, given any elements xx and yy of SS, x=yx = y whenever S *xS \downarrow^* x and S *yS \downarrow^* y are isomorphic as pointed sets equipped with a relation \prec.

Note that this definition includes weak extensionality, which won't follow from the other half unless \prec is well-founded (see the examples below). It is possible to get weak extensionality free by using the transitive closure +\prec^+ instead; that is, define S +yS \downarrow^+ y with n>0n \gt 0 only. But then you need another step; define (S +y) (S \downarrow^+ y)^\top to be a pointed set with a new point \top adjoined to S +yS \downarrow^+ y; let xx \prec \top if and only if xyx \prec y in SS itself. (For a well-founded relation, (S +y) S *y(S \downarrow^+ y)^\top \cong S \downarrow^* y; in general, however, yy may already belong to S +yS \downarrow^+ y, yet yy \ne \top in (S +y) (S \downarrow^+ y)^\top.) Then \prec is Finsler-extensional on SS if and only if x=yx = y whenever (S +x) (S +y) (S \downarrow^+ x)^\top \cong (S \downarrow^+ y)^\top as pointed sets equipped with \prec.

It is immediate that Finsler extensionality implies weak extensionality; the converse may be proved (using induction) for well-founded relations.

Scott extensionality

Given an element yy of SS, let a path to yy consist of a sequence

x=t 0t n=y x = t_0 \prec \cdots \prec t_n = y

for n0n \geq 0. Then let T yT_y be the set of paths to yy; given paths t\vec{t} and u\vec{u} in N yN_y, say that tu\vec{t} \to \vec{u} if u=(t 1,,t m)\vec{u} = (t_1, \ldots, t_m) for some mnm \leq n. Then T yT_y with the relation \to is the tree to yy.

SS is Scott-extensional if the only automorphism of any such tree T yT_y (as a set equipped with a relation \to) is the identity function on T yT_y.

Then Scott extensionality implies Finsler extensionality, and the converse holds for well-founded relations.

Strong extensionality

The strongest version of extensionality is motivated by the study of terminal coalgebras and coinduction.

Let SS be equipped with a binary relation \prec. A bisimulation on (S,)(S,\prec) is a binary relation \sim such that whenever xyx \sim y, for any axa \prec x there is a byb \prec y with aba \sim b, and conversely for every byb \prec y there is an axa \prec x with again aba \sim b. We then say that \prec is strongly extensional if every bisimulation is contained in the identity relation; i.e., x=yx = y whenever xyx \sim y for any bisimulation \sim. In general, this is probably the best situation in which to say that \prec is simply extensional.

Finsler and Scott extensionality may be understood as special cases of this for particular bisimulations \sim. (So can strong extensionality, since any set equipped with a relation has a weakest bisimulation \approx.) This is the approach taken by Aczel to study all the above notions of extensionality together.

In particular, strong extensionality implies Scott extensionality, and the converse holds for well-founded relations. Thus, all forms of extensionality are equivalent for well-founded relations.

Weak extensionality for arbitrary binary relations

Given sets AA and BB, let \prec be a binary relation on AA and BB, or equivalently, a predicate on the cartesian product A×BA \times B. Then \prec is (weakly) extensional if, given any elements xx and yy of BB, x= Byx =_B y whenever for all t:At:A, txt \prec x if and only if tyt \prec y.

x:B.y:B.(x= By)t:A.(tx)(ty)\forall x:B.\forall y:B.(x =_B y) \iff \forall t:A.(t \prec x) \iff (t \prec y)

In homotopy type theory

In homotopy type theory, a relation is an h-proposition-valued type family. A binary relation \prec on a carrier type SS is weakly extensional if for all terms a:Sa:S and b:Sb:S the canonical function

idtoextcond(a,b):(a= Sb) c:S(ca)(cb)\mathrm{idtoextcond}(a, b):(a =_S b) \to \prod_{c:S} (c \prec a) \simeq (c \prec b)

is an equivalence of types. This implies that the type SS is an h-set.

Examples

  • The axiom of extensionality in material set theory states membership is an extensional relation on the class of pure sets. (Note that the axiom of foundation states that membership is a well-founded relation, so one usually doesn't worry about the different notions of extensionality for ill-founded relations.) More generally, the membership relation on the transitive closure or reflexive-transitive closure of a pure set is an extensional relation on a set.

  • Conversely, one can define pure sets in structural set theory in part as sets equipped with an extensional (and optionally well-founded) relation.

  • In any single-sorted definition of a topos, there is a terminal object 11 (represented by the identity morphism of the terminal object), one could define the relation \prec on the set of morphisms CC as

abs(a)=1t(b)=1t(a)=s(b)a \prec b \coloneqq s(a) = 1 \wedge t(b) = 1 \wedge t(a) = s(b)

Due to the universal property of the terminal object, \prec is weakly extensional. However, \prec is not strongly extensional. The relation \sim defined by equality on every pair of functions aba=ba \sim b \coloneqq a = b, and in addition, id 2swap\mathrm{id}_2 \sim \mathrm{swap} and swapid 2\mathrm{swap} \sim \mathrm{id}_2 for the identity function and the swap function on the set with two elements 22, is a bisimulation on \prec, but it is not true that id 2=swap\mathrm{id}_2 = \mathrm{swap}.

abs(a)=1s(b)=0t(a)=t(b)a \in b \coloneqq s(a) = 1 \wedge s(b) = 0 \wedge t(a) = t(b)

Due to the universal property of the initial object, \in is weakly extensional. However, \in is not strongly extensional, for the same reason that \prec defined above is not strongly extensional.

  • A well-order is precisely a well-founded, transitive, extensional relation. Removing well-foundedness here gives a theory of ill-founded ordinal numbers.

  • On the set 2={0,1}\mathbf{2} = \{0,1\}, now let 000 \prec 0 and 010 \prec 1 (but no other relationships). This relation is not weakly extensional, although it does satisfy the other half of Finsler extensionality, since 2 *02 *1\mathbf{2} \downarrow^* 0 \ncong \mathbf{2} \downarrow^* 1. However, (2 +0) (2 +1) (\mathbf{2} \downarrow^+ 0)^\top \cong (\mathbf{2} \downarrow^+ 1)^\top; this shows the necessity of defining Finsler extensionality as we do.

  • On the set 2\mathbf{2} again, let 010 \prec 1 and 101 \prec 0 (but 000 \nprec 0 and 111 \nprec 1). This relation is weakly extensional but not Finsler-extensional, since 2 *02 *1\mathbf{2} \downarrow^* 0 \cong \mathbf{2} \downarrow^* 1. Yet 00 and 11 can hardly be distinguished by \prec when there is an automorphism of (2,)(\mathbf{2},\prec) that swaps them; this and the other examples below motivate the stronger notions of extensionality.

  • On the set 3={0,1,2}\mathbf{3} = \{0,1,2\}, let 202 \nprec 0 and iii \nprec i but all other relationships hold. Then this relation is Finsler-extensional but not Scott-extensional, since T 2T 1T_2 \cong T_1.

  • Finally, on the set 2\mathbf{2} again, let 101 \nprec 0 but all other relationships hold. Then this relation is Scott-extensional but not strongly extensional, since 010 \approx 1.

Extensional quotients

Weak extensionality is a kind of antisymmetry condition: Let xyx \leq y mean that tyt \prec y whenever txt \prec x. Then \leq is clearly a preorder, which is antisymmetric (so a partial order) if and only if \prec is weakly extensional.

Now suppose that if txt \prec x if and only if tyt \prec y for all tt, then xzx \prec z if and only if yzy \prec z for all zz. Then if we define xyx \equiv y to mean that xyx \leq y and yxy \leq x, then \equiv is an equivalence relation such that \prec descends to a weakly extensional relation on the quotient set S/S/{\equiv}.

Strongly extensional quotients are even easier to construct, although they do create additional relationships. It is easy to see that the union of any family of bisimulations is a bisimulation, and therefore there is a largest bisimulation \approx for any binary relation \prec on SS. Moreover, \approx is an equivalence relation (though not every bisimulation need be so), and \prec descends to a strongly extensional relation on the quotient S/S/\approx.

Simulations

Given two sets SS and TT, each equipped with a strongly extensional relation \prec, a function f:STf\colon S \to T is a simulation of SS in TT if

  • f(x)f(y)f(x) \prec f(y) whenever xyx \prec y and
  • given tf(x)t \prec f(x), there exists yxy \prec x with t=f(y)t = f(y).

Then sets so equipped form a category with simulations as morphisms.

Note that there is at most one simulation from SS to TT; in fact, strong extensionality for TT is equivalent to saying that any two simulations STS \rightrightarrows T are equal. Also, any simulation from SS to TT must be an injection; in fact, strong extensionality for SS is equivalent to saying that any simulation STS \to T is injective.

Thus, we have a (large) poset of sets equipped with extensional relations, and we can consistently interpret the simulations as subset inclusion. This leads to the model of sets equipped with extensional relations as transitive sets.

References

For extensional relations in homotopy type theory, see

Last revised on October 24, 2022 at 20:59:56. See the history of this page for a list of all contributions to it.